T:Type, as, bs:T List. as  bs  bs  as  as = bs 

latex

Definitions	{T}, P  Q, l1  l2, b, null(as), Prop, False, P  Q, P & Q, x:A. B(x), P  Q, t  T
Lemmas	cons iseg, null wf, assert wf, iseg wf, iseg nil, implies functionality wrt iff